﻿// Jinx AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Formality.FormalSystem;
using Core;

namespace Formality.Game
{
    public enum ResponseType
    {
        Rejected,
        Accepted,
        Proved,
        Finished
    }

    public class ActiveGame<T>
        where T : class
    {
        private readonly Engine<T> Engine;
        private int Counter;
        private Sentence<T> goal;
        private List<Submission<T>> submissionList;

        public ActiveGame(Engine<T> Engine, IPlayer<T> Player)
        {
            this.Engine = Engine;
            Goal = Engine[Player.ProblemId];

            this.Player = Player;
        }

        public IPlayer<T> Player { get; private set; }

        public Sentence<T> Goal
        {
            get { return goal; }
            set
            {
                submissionList = new List<Submission<T>>();
                goal = value;
                Counter = 0;

                if (Player != null)
                    Player.ChangeGoal(value.Id);
            }
        }

        public IEnumerable<Submission<T>> Submissions
        {
            get
            {
                foreach (var S in submissionList)
                    yield return S;
            }
        }

        public IEnumerable<Sentence<T>> Premises
        {
            get { return Engine.GetPremises(goal.Id); }
        }

        public IEnumerable<Submission<T>> Prime()
        {
            foreach (var Sub in Player.CurrentProblemSubmissions)
            {
                if (Sub == "(z = x ≡ z = y) → (∀φ (φ!z ≡ φ!x) ≡ z = y)")
                    Console.WriteLine();

                Inference? Inference;
                Sentence<T> Parsed;

                Follows(Sub, out Parsed, out Inference);

                var Resp = Inference.HasValue
                               ? ResponseType.Accepted
                               : ResponseType.Rejected;

                var Submission = new Submission<T>(Parsed, Resp, Inference);

                submissionList.Add(Submission);

                yield return Submission;
            }
        }

        public Submission<T> Submit(string Input)
        {
            Sentence<T> Parsed;
            Inference? Inference;

            Follows(Input, out Parsed, out Inference);

            var Resp = UpdateState(Parsed, Inference);
            var Sub = new Submission<T>(Parsed, Resp, Inference);

            if (Resp == ResponseType.Accepted
                || Resp == ResponseType.Rejected)
                submissionList.Add(Sub);

            return Sub;
        }

        private void Follows(string Input, out Sentence<T> Sentence, out Inference? Inference)
        {
            if (Input == "prop")
                Input = Goal.Item.ToString();

            if (DidGoto(Input))
            {
                Sentence = null;
                Inference = null;
                return;
            }

            var Parsed = Engine.Parse(Input);

            if (!Engine.IsGoal(Parsed))
                throw new Exception("You must enter a proposition");

            var Id = "(" + ++Counter + ")";
            Sentence = new Sentence<T>(Id, Id, Parsed);

            var Given = (from P in Premises
                         select Tuple.New(P.Item, false));

            var WorkingPremises = Given.Concat
                       (from S in submissionList
                        where S.Response == ResponseType.Accepted
                        select Tuple.New(S.Sentence.Item, true));

            Inference = Engine.Follows(Parsed, Enumerable.Reverse(WorkingPremises));
        }

        private bool DidGoto(string Input)
        {
            var GotoCommand = "goto ";

            if (Input.StartsWith(GotoCommand))
            {
                Input = Input.Remove(0, GotoCommand.Length);

                Goal = Engine[Input];

                return true;
            }

            return false;
        }

        private ResponseType UpdateState(Sentence<T> Parsed, Inference? Inference)
        {
            ResponseType Resp;
            if (Inference.HasValue)
            {
                if (Player != null)
                    Player.AddSubmission(Parsed, Counter);

                if (Parsed.Item.Equals(Goal.Item) == false)
                {
                    Resp = ResponseType.Accepted;
                }
                else
                {
                    Resp = ResponseType.Proved;

                    var NextId = Engine.Next(Goal.Id);

                    if (NextId != null)
                    {
                        Goal = Engine[NextId];
                    }
                    else
                    {
                        Resp = ResponseType.Finished;
                        goal = null;
                    }
                }
            }
            else
            {
                Resp = ResponseType.Rejected;
            }
            return Resp;
        }

        public override string ToString()
        {
            var Buffer = new StringBuilder();

            Buffer.AppendFormat("Game with {0}\n", Player.Name);

            foreach (var P in Premises)
                Buffer.AppendFormat("\t{0}\t{1}\n", P.Name, P.Item);

            foreach (var Sub in submissionList)
                Buffer.AppendFormat("\t{1}\t{0}\n", Sub.Sentence.Item, Status(Sub));

            Buffer.AppendFormat("Goal: {1} {0}\n", Goal.Item, Goal.Name);

            return Buffer.ToString();
        }

        private static string Status(Submission<T> Sub)
        {
            switch (Sub.Response)
            {
                case ResponseType.Finished:
                    return "YOU WON";
                case ResponseType.Proved:
                    return "QED";
                case ResponseType.Rejected:
                    return "!";
            }

            return Sub.Sentence.Name;
        }
    }
}